\functions {
int x1;
int x4;
int x9;
int x2;
int x5;
int x7;
int x6;
int x3;
int x8;
int x0;
}
\predicates {
}
\problem {
\part[P1]((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((v_princess_55() & (((!((v_princess_50() & (((0) <= (v_princess_54)))))) -> (!(v_princess_55()))) & (((v_princess_50() & (((0) <= (v_princess_54))))) -> (v_princess_55())))))) & (v_princess_54) = ((v_princess_53+x4))))) & (v_princess_53) = ((v_princess_52+x5))))) & (v_princess_52) = ((v_princess_3+v_princess_51))))) & (v_princess_51) = ((x9*((0) - (2))))))) & (((!((v_princess_45() & (((0) <= (v_princess_49)))))) -> (!(v_princess_50()))) & (((v_princess_45() & (((0) <= (v_princess_49))))) -> (v_princess_50())))))) & (v_princess_49) = ((v_princess_48+x4))))) & (v_princess_48) = ((v_princess_47+v_princess_5))))) & (v_princess_47) = ((v_princess_46+v_princess_18))))) & (v_princess_46) = ((v_princess_3+v_princess_15))))) & (((!((v_princess_40() & (((0) <= (v_princess_44)))))) -> (!(v_princess_45()))) & (((v_princess_40() & (((0) <= (v_princess_44))))) -> (v_princess_45())))))) & (v_princess_44) = ((v_princess_43+x5))))) & (v_princess_43) = ((v_princess_42+v_princess_26))))) & (v_princess_42) = ((v_princess_41+x1))))) & (v_princess_41) = ((x0+v_princess_30))))) & (((!((v_princess_36() & (((0) <= (v_princess_39)))))) -> (!(v_princess_40()))) & (((v_princess_36() & (((0) <= (v_princess_39))))) -> (v_princess_40())))))) & (v_princess_39) = ((v_princess_38+x7))))) & (v_princess_38) = ((v_princess_37+x5))))) & (v_princess_37) = ((x6+v_princess_3))))) & (((!((v_princess_29() & (((v_princess_35) <= (0)))))) -> (!(v_princess_36()))) & (((v_princess_29() & (((v_princess_35) <= (0))))) -> (v_princess_36())))))) & (v_princess_35) = ((v_princess_34+x4))))) & (v_princess_34) = ((v_princess_32+v_princess_33))))) & (v_princess_33) = ((x7*((0) - (1))))))) & (v_princess_32) = ((v_princess_31+x9))))) & (v_princess_31) = ((v_princess_3+v_princess_30))))) & (v_princess_30) = ((x8*((0) - (1))))))) & (((!((v_princess_23() & (((v_princess_28) <= (((0) - (1)))))))) -> (!(v_princess_29()))) & (((v_princess_23() & (((v_princess_28) <= (((0) - (1))))))) -> (v_princess_29())))))) & (v_princess_28) = ((v_princess_27+x4))))) & (v_princess_27) = ((v_princess_25+v_princess_26))))) & (v_princess_26) = ((x3*((0) - (1))))))) & (v_princess_25) = ((v_princess_24+x8))))) & (v_princess_24) = ((x0+x2))))) & (((!((v_princess_22() & (((x0) <= (x8)))))) -> (!(v_princess_23()))) & (((v_princess_22() & (((x0) <= (x8))))) -> (v_princess_23())))))) & (((!((v_princess_14() & (((1) <= (v_princess_21)))))) -> (!(v_princess_22()))) & (((v_princess_14() & (((1) <= (v_princess_21))))) -> (v_princess_22())))))) & (v_princess_21) = ((v_princess_20+x4))))) & (v_princess_20) = ((v_princess_19+x3))))) & (v_princess_19) = ((v_princess_17+v_princess_18))))) & (v_princess_18) = ((x1*((0) - (1))))))) & (v_princess_17) = ((v_princess_16+x8))))) & (v_princess_16) = ((x0+v_princess_15))))) & (v_princess_15) = ((x2*((0) - (1))))))) & (((!((v_princess_11() & (((v_princess_13) <= (0)))))) -> (!(v_princess_14()))) & (((v_princess_11() & (((v_princess_13) <= (0))))) -> (v_princess_14())))))) & (v_princess_13) = ((v_princess_12+x3))))) & (v_princess_12) = ((x0+x1))))) & (((!(((((0) <= (v_princess_2))) & (((v_princess_10) <= (0)))))) -> (!(v_princess_11()))) & ((((((0) <= (v_princess_2))) & (((v_princess_10) <= (0))))) -> (v_princess_11())))))) & (v_princess_10) = ((v_princess_8+v_princess_9))))) & (v_princess_9) = ((x4*2))))) & (v_princess_8) = ((v_princess_6+v_princess_7))))) & (v_princess_7) = ((x5*((0) - (1))))))) & (v_princess_6) = ((v_princess_4+v_princess_5))))) & (v_princess_5) = ((x9*((0) - (1))))))) & (v_princess_4) = ((v_princess_3+x3))))) & (v_princess_3) = ((x0*((0) - (1)))))))) & (v_princess_2) = ((v_princess_1+x9))))) & (v_princess_1) = ((v_princess_0+x1))))) & (v_princess_0) = ((x0+x8))))))
 &
\part[P2](((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((v_princess_144() & (((!((v_princess_137() & (((((0) - (1))) <= (v_princess_143)))))) -> (!(v_princess_144()))) & (((v_princess_137() & (((((0) - (1))) <= (v_princess_143))))) -> (v_princess_144())))))) & (v_princess_143) = ((v_princess_142+x4))))) & (v_princess_142) = ((v_princess_141+v_princess_71))))) & (v_princess_141) = ((v_princess_140+x5))))) & (v_princess_140) = ((v_princess_139+v_princess_67))))) & (v_princess_139) = ((v_princess_138+v_princess_80))))) & (v_princess_138) = ((v_princess_56+v_princess_64))))) & (((!((v_princess_134() & (((v_princess_136) <= (((0) - (1)))))))) -> (!(v_princess_137()))) & (((v_princess_134() & (((v_princess_136) <= (((0) - (1))))))) -> (v_princess_137())))))) & (v_princess_136) = ((v_princess_135+x4))))) & (v_princess_135) = ((x6+x1))))) & (((!((v_princess_132() & (((v_princess_133) <= (0)))))) -> (!(v_princess_134()))) & (((v_princess_132() & (((v_princess_133) <= (0))))) -> (v_princess_134())))))) & (v_princess_133) = ((v_princess_125+x7))))) & (((!((v_princess_129() & (((1) <= (v_princess_131)))))) -> (!(v_princess_132()))) & (((v_princess_129() & (((1) <= (v_princess_131))))) -> (v_princess_132())))))) & (v_princess_131) = ((v_princess_130+x7))))) & (v_princess_130) = ((x8*((0) - (2))))))) & (((!((v_princess_124() & (((v_princess_128) <= (0)))))) -> (!(v_princess_129()))) & (((v_princess_124() & (((v_princess_128) <= (0))))) -> (v_princess_129())))))) & (v_princess_128) = ((v_princess_127+x7))))) & (v_princess_127) = ((v_princess_126+x5))))) & (v_princess_126) = ((v_princess_125+v_princess_65))))) & (v_princess_125) = ((v_princess_56+v_princess_80))))) & (((!((v_princess_119() & (((v_princess_123) <= (0)))))) -> (!(v_princess_124()))) & (((v_princess_119() & (((v_princess_123) <= (0))))) -> (v_princess_124())))))) & (v_princess_123) = ((v_princess_122+x7))))) & (v_princess_122) = ((v_princess_121+x5))))) & (v_princess_121) = ((v_princess_120+v_princess_67))))) & (v_princess_120) = ((x2+x1))))) & (((!((v_princess_115() & (((0) <= (v_princess_118)))))) -> (!(v_princess_119()))) & (((v_princess_115() & (((0) <= (v_princess_118))))) -> (v_princess_119())))))) & (v_princess_118) = ((v_princess_117+x7))))) & (v_princess_117) = ((v_princess_116+v_princess_69))))) & (v_princess_116) = ((v_princess_65+v_princess_67))))) & (((!((v_princess_110() & (((v_princess_114) <= (0)))))) -> (!(v_princess_115()))) & (((v_princess_110() & (((v_princess_114) <= (0))))) -> (v_princess_115())))))) & (v_princess_114) = ((v_princess_113+x9))))) & (v_princess_113) = ((v_princess_111+v_princess_112))))) & (v_princess_112) = ((x8*((0) - (1))))))) & (v_princess_111) = ((x6+v_princess_64))))) & (((!((v_princess_107() & (((1) <= (v_princess_109)))))) -> (!(v_princess_110()))) & (((v_princess_107() & (((1) <= (v_princess_109))))) -> (v_princess_110())))))) & (v_princess_109) = ((v_princess_108+x5))))) & (v_princess_108) = ((x6+x3))))) & (((!((v_princess_103() & (((v_princess_106) <= (0)))))) -> (!(v_princess_107()))) & (((v_princess_103() & (((v_princess_106) <= (0))))) -> (v_princess_107())))))) & (v_princess_106) = ((v_princess_105+x7))))) & (v_princess_105) = ((v_princess_104+v_princess_67))))) & (v_princess_104) = ((x6+x8))))) & (((!((v_princess_100() & (((1) <= (v_princess_102)))))) -> (!(v_princess_103()))) & (((v_princess_100() & (((1) <= (v_princess_102))))) -> (v_princess_103())))))) & (v_princess_102) = ((v_princess_101+x4))))) & (v_princess_101) = ((v_princess_64+v_princess_71))))) & (((!((v_princess_96() & (((0) <= (v_princess_99)))))) -> (!(v_princess_100()))) & (((v_princess_96() & (((0) <= (v_princess_99))))) -> (v_princess_100())))))) & (v_princess_99) = ((v_princess_98+x7))))) & (v_princess_98) = ((v_princess_97+x3))))) & (v_princess_97) = ((v_princess_64+v_princess_80))))) & (((!((v_princess_93() & (((((0) - (1))) <= (v_princess_95)))))) -> (!(v_princess_96()))) & (((v_princess_93() & (((((0) - (1))) <= (v_princess_95))))) -> (v_princess_96())))))) & (v_princess_95) = ((v_princess_94+x5))))) & (v_princess_94) = ((x2+v_princess_80))))) & (((!((v_princess_91() & (((v_princess_92) <= (0)))))) -> (!(v_princess_93()))) & (((v_princess_91() & (((v_princess_92) <= (0))))) -> (v_princess_93())))))) & (v_princess_92) = ((v_princess_81+x4))))) & (((!((v_princess_88() & (((1) <= (v_princess_90)))))) -> (!(v_princess_91()))) & (((v_princess_88() & (((1) <= (v_princess_90))))) -> (v_princess_91())))))) & (v_princess_90) = ((v_princess_89+x4))))) & (v_princess_89) = ((x2+x8))))) & (((!((v_princess_87() & (((x3) <= (((0) - (1)))))))) -> (!(v_princess_88()))) & (((v_princess_87() & (((x3) <= (((0) - (1))))))) -> (v_princess_88())))))) & (((!((v_princess_85() & (((v_princess_86) <= (1)))))) -> (!(v_princess_87()))) & (((v_princess_85() & (((v_princess_86) <= (1))))) -> (v_princess_87())))))) & (v_princess_86) = ((v_princess_56+x9))))) & (((!((v_princess_79() & (((0) <= (v_princess_84)))))) -> (!(v_princess_85()))) & (((v_princess_79() & (((0) <= (v_princess_84))))) -> (v_princess_85())))))) & (v_princess_84) = ((v_princess_83+x7))))) & (v_princess_83) = ((v_princess_81+v_princess_82))))) & (v_princess_82) = ((x5*2))))) & (v_princess_81) = ((x6+v_princess_80))))) & (v_princess_80) = ((x1*((0) - (1))))))) & (((!((v_princess_75() & (((0) <= (v_princess_78)))))) -> (!(v_princess_79()))) & (((v_princess_75() & (((0) <= (v_princess_78))))) -> (v_princess_79())))))) & (v_princess_78) = ((v_princess_76+v_princess_77))))) & (v_princess_77) = ((x7*2))))) & (v_princess_76) = ((x6+v_princess_65))))) & (((!((v_princess_74() & (((x3) <= (x4)))))) -> (!(v_princess_75()))) & (((v_princess_74() & (((x3) <= (x4))))) -> (v_princess_75())))))) & (((!((v_princess_63() & (((v_princess_73) <= (0)))))) -> (!(v_princess_74()))) & (((v_princess_63() & (((v_princess_73) <= (0))))) -> (v_princess_74())))))) & (v_princess_73) = ((v_princess_72+x4))))) & (v_princess_72) = ((v_princess_70+v_princess_71))))) & (v_princess_71) = ((x7*((0) - (1))))))) & (v_princess_70) = ((v_princess_68+v_princess_69))))) & (v_princess_69) = ((x5*((0) - (1))))))) & (v_princess_68) = ((v_princess_66+v_princess_67))))) & (v_princess_67) = ((x9*((0) - (1))))))) & (v_princess_66) = ((v_princess_64+v_princess_65))))) & (v_princess_65) = ((x3*((0) - (1))))))) & (v_princess_64) = ((x2*((0) - (1))))))) & (((!((v_princess_62() & (((x6) <= (0)))))) -> (!(v_princess_63()))) & (((v_princess_62() & (((x6) <= (0))))) -> (v_princess_63())))))) & (((!(((((v_princess_59) <= (1))) & (((v_princess_61) <= (0)))))) -> (!(v_princess_62()))) & ((((((v_princess_59) <= (1))) & (((v_princess_61) <= (0))))) -> (v_princess_62())))))) & (v_princess_61) = ((x1+v_princess_60))))) & (v_princess_60) = ((x9*2)))))) & (v_princess_59) = ((v_princess_58+x8))))) & (v_princess_58) = ((v_princess_56+v_princess_57))))) & (v_princess_57) = ((x2*((0) - (2))))))) & (v_princess_56) = ((x6*((0) - (1))))))))
 -> false
}
\functions {
int v_princess_143;
int v_princess_142;
int v_princess_141;
int v_princess_140;
int v_princess_139;
int v_princess_138;
int v_princess_136;
int v_princess_135;
int v_princess_133;
int v_princess_131;
int v_princess_130;
int v_princess_128;
int v_princess_127;
int v_princess_126;
int v_princess_125;
int v_princess_123;
int v_princess_122;
int v_princess_121;
int v_princess_120;
int v_princess_118;
int v_princess_117;
int v_princess_116;
int v_princess_114;
int v_princess_113;
int v_princess_112;
int v_princess_111;
int v_princess_109;
int v_princess_108;
int v_princess_106;
int v_princess_105;
int v_princess_104;
int v_princess_102;
int v_princess_101;
int v_princess_99;
int v_princess_98;
int v_princess_97;
int v_princess_95;
int v_princess_94;
int v_princess_92;
int v_princess_90;
int v_princess_89;
int v_princess_86;
int v_princess_84;
int v_princess_83;
int v_princess_82;
int v_princess_81;
int v_princess_80;
int v_princess_78;
int v_princess_77;
int v_princess_76;
int v_princess_73;
int v_princess_72;
int v_princess_71;
int v_princess_70;
int v_princess_69;
int v_princess_68;
int v_princess_67;
int v_princess_66;
int v_princess_65;
int v_princess_64;
int v_princess_61;
int v_princess_60;
int v_princess_59;
int v_princess_58;
int v_princess_57;
int v_princess_56;
int v_princess_54;
int v_princess_53;
int v_princess_52;
int v_princess_51;
int v_princess_49;
int v_princess_48;
int v_princess_47;
int v_princess_46;
int v_princess_44;
int v_princess_43;
int v_princess_42;
int v_princess_41;
int v_princess_39;
int v_princess_38;
int v_princess_37;
int v_princess_35;
int v_princess_34;
int v_princess_33;
int v_princess_32;
int v_princess_31;
int v_princess_30;
int v_princess_28;
int v_princess_27;
int v_princess_26;
int v_princess_25;
int v_princess_24;
int v_princess_21;
int v_princess_20;
int v_princess_19;
int v_princess_18;
int v_princess_17;
int v_princess_16;
int v_princess_15;
int v_princess_13;
int v_princess_12;
int v_princess_10;
int v_princess_9;
int v_princess_8;
int v_princess_7;
int v_princess_6;
int v_princess_5;
int v_princess_4;
int v_princess_3;
int v_princess_2;
int v_princess_1;
int v_princess_0;
}
\predicates {
v_princess_144;
v_princess_137;
v_princess_134;
v_princess_132;
v_princess_129;
v_princess_124;
v_princess_119;
v_princess_115;
v_princess_110;
v_princess_107;
v_princess_103;
v_princess_100;
v_princess_96;
v_princess_93;
v_princess_91;
v_princess_88;
v_princess_87;
v_princess_85;
v_princess_79;
v_princess_75;
v_princess_74;
v_princess_63;
v_princess_62;
v_princess_55;
v_princess_50;
v_princess_45;
v_princess_40;
v_princess_36;
v_princess_29;
v_princess_23;
v_princess_22;
v_princess_14;
v_princess_11;
}
// \interpolant { P1; P2 }
